Nuprl Lemma : s-insert_wf 11,40

T:Type. subtype_rel(T (x:TL:(T List). s-insert(xL (T List)) 
latex


Definitionst  T, x:AB(x), i <z j, if b then t else f fi , (i = j), s-insert(xl), P  Q
Lemmaseq int wf, ifthenelse wf, lt int wf

origin